fact DamageRuleset  {
    all w, w' :World, d:Property | ( 
        (
			(w' in w.next) 
			and (
				some d0:Object |(d0 in w.exists) and (d0 in w'.exists)
				and ((d in w.Damage) iff (d not in w'.Damage))
				and ((d->d0 in w.hasDamage) or (d->d0 in w'.hasDamage))
			)
		) => ( 
            (some shared_r:Object |(w.CreateDamageRule_before[d, shared_r] and w'.CreateDamageRule_after[d, shared_r]))
            or (some shared_c:Object |(w.DeleteDamageRule_before[d, shared_c] and w'.DeleteDamageRule_after[d, shared_c]))
        )
    )
}

pred World.CreateDamageRule_before[d:Property, shared_r:Object] {
    disj[d, shared_r] 
    and(shared_r in this.RentedCar)
    and (d not in this.Damage)
}

pred World.CreateDamageRule_after[d:Property, shared_r:Object] {
    disj[d, shared_r] 
    and(shared_r in this.Car)
    and (shared_r in this.RentedCar)
    and (shared_r in this.Damaged)
    and (d in this.Damage)
    and (shared_r in this.RentalCar)
    and (d -> shared_r in this.hasDamage)
}

pred World.DeleteDamageRule_before[d:Property, shared_c:Object] {
    disj[d, shared_c] 
    and(shared_c in this.RentalCar)
    and (shared_c in this.Damaged)
    and (shared_c in this.Car)
    and (d -> shared_c in this.hasDamage)
    and (shared_c in this.CarUnderMaintenance)
    and (d in this.Damage)
}

pred World.DeleteDamageRule_after[d:Property, shared_c:Object] {
    disj[d, shared_c] 
    and(d not in this.Damage)
    and (shared_c in this.Car)
}


fact AgreementRuleset  {
    all w, w' :World, a:Property | ( 
        not( 
            (w' in w.next) 
            and ( no p:Object | ((a -> p in w.proprietorOwnsOffice) and (p not in w'.exists)))
            and ( no b:Object | ((a -> b in w.officeUsedByProprietor) and (b not in w'.exists)))
            and ((a in w.Agreement) iff (a not in w'.Agreement))
            
        )
    )
}


fact OwnershipRuleset  {
    all w, w' :World, o:Property | ( 
        not( 
            (w' in w.next) 
            and ( no r:Object | ((o -> r in w.carOwnedByCompany) and (r not in w'.exists)))
            and ( no o0:Object | ((o -> o0 in w.companyOwnsCar) and (o0 not in w'.exists)))
            and ((o in w.Ownership) iff (o not in w'.Ownership))
            
        )
    )
}


fact RentalContractRuleset  {
    all w, w' :World, r0:Property | ( 
        (
			(w' in w.next) 
			and ( no c:Object | ((r0 -> c in w.customerRentsCar) and (c not in w'.exists)))
			and ( no r1:Object | ((r0 -> r1 in w.carIsRented) and (r1 not in w'.exists)))
			and ((r0 in w.RentalContract) iff (r0 not in w'.RentalContract))
			
		) => ( 
            (some shared_r0:Object |(w.CreateRentalContractRule_before[r0, shared_r0] and w'.CreateRentalContractRule_after[r0, shared_r0]))
            or ((w.DeleteRentalContractRule_before[r0] and w'.DeleteRentalContractRule_after[r0]))
        )
    )
}

pred World.CreateRentalContractRule_before[r0:Property, shared_r0:Object] {
    disj[r0, shared_r0] 
    and(shared_r0 in this.RentalCar)
    and (r0 not in this.RentalContract)
    and (shared_r0 in this.StoredCar)
}

pred World.CreateRentalContractRule_after[r0:Property, shared_r0:Object] {
    disj[r0, shared_r0] 
    and(shared_r0 in this.Undamaged)
    and (shared_r0 in this.Car)
    and (r0 -> shared_r0 in this.carIsRented)
    and (r0 in this.RentalContract)
    and (shared_r0 in this.RentedCar)
    and (shared_r0 in this.RentalCar)
}

pred World.DeleteRentalContractRule_before[r0:Property] {
    (r0 in this.RentalContract)
}

pred World.DeleteRentalContractRule_after[r0:Property] {
    (r0 not in this.RentalContract)
}


fact ParkingRuleset  {
    all w, w' :World, p0:Property | ( 
        (
			(w' in w.next) 
			and ( no p1:Object | ((p0 -> p1 in w.officeUsedForParking) and (p1 not in w'.exists)))
			and ( no s:Object | ((p0 -> s in w.carStoredAtOffice) and (s not in w'.exists)))
			and ((p0 in w.Parking) iff (p0 not in w'.Parking))
			
		) => ( 
            ((w.CreateParkingRule_before[p0] and w'.CreateParkingRule_after[p0]))
            or (some shared_r1:Object |(w.DeleteParkingRule_before[p0, shared_r1] and w'.DeleteParkingRule_after[p0, shared_r1]))
        )
    )
}

pred World.CreateParkingRule_before[p0:Property] {
    (p0 not in this.Parking)
}

pred World.CreateParkingRule_after[p0:Property] {
    (p0 in this.Parking)
}

pred World.DeleteParkingRule_before[p0:Property, shared_r1:Object] {
    disj[p0, shared_r1] 
    and(p0 -> shared_r1 in this.carStoredAtOffice)
    and (shared_r1 in this.StoredCar)
    and (p0 in this.Parking)
    and (shared_r1 in this.RentalCar)
}

pred World.DeleteParkingRule_after[p0:Property, shared_r1:Object] {
    disj[p0, shared_r1] 
    and(p0 not in this.Parking)
    and (shared_r1 in this.RentalCar)
    and (shared_r1 in this.RentedCar)
}


fact damagePhaseRuleset  {
    all w, w' :World, d1:Object | ( 
        not( 
            (w' in w.next) 
            and ((d1 in w.Car) and (d1 in w'.Car)) 
            and not((d1 in w.Damaged) and (d1 in w'.Damaged))
            and not((d1 in w.Undamaged) and (d1 in w'.Undamaged))
        )
    )
}


fact PersonRuleset  {
    all w, w' :World, p2:Object | ( 
        (
			(w' in w.next) 
			and ((p2 in w.Person) iff (p2 not in w'.Person))
		) => ( 
            ((w.CreatePersonRule_before[p2] and w'.CreatePersonRule_after[p2]))
            or ((w.DeletePersonRule_before[p2] and w'.DeletePersonRule_after[p2]))
        )
    )
}

pred World.CreatePersonRule_before[p2:Object] {
    (p2 not in this.Person)
}

pred World.CreatePersonRule_after[p2:Object] {
    (p2 in this.Customer)
    and (p2 in this.Person)
}

pred World.DeletePersonRule_before[p2:Object] {
    (p2 not in this.Customer)
    and (p2 in this.Person)
}

pred World.DeletePersonRule_after[p2:Object] {
    (p2 not in this.Person)
}


fact MaintenanceRuleset  {
    all w, w' :World, m:Property | ( 
        (
			(w' in w.next) 
			and ( no c0:Object | ((m -> c0 in w.carMaintainedByGarage) and (c0 not in w'.exists)))
			and ( no g:Object | ((m -> g in w.garageUsedForMaintenance) and (g not in w'.exists)))
			and ((m in w.Maintenance) iff (m not in w'.Maintenance))
			
		) => ( 
            (some shared_c0:Object |(w.CreateMaintenanceRule_before[m, shared_c0] and w'.CreateMaintenanceRule_after[m, shared_c0]))
            or ((w.DeleteMaintenanceRule_before[m] and w'.DeleteMaintenanceRule_after[m]))
        )
    )
}

pred World.CreateMaintenanceRule_before[m:Property, shared_c0:Object] {
    disj[m, shared_c0] 
    and(m not in this.Maintenance)
    and (shared_c0 in this.Damaged)
    and (shared_c0 in this.Car)
}

pred World.CreateMaintenanceRule_after[m:Property, shared_c0:Object] {
    disj[m, shared_c0] 
    and(m in this.Maintenance)
    and (shared_c0 in this.CarUnderMaintenance)
    and (shared_c0 in this.Car)
    and (shared_c0 in this.RentalCar)
    and (shared_c0 in this.Damaged)
    and (m -> shared_c0 in this.carMaintainedByGarage)
}

pred World.DeleteMaintenanceRule_before[m:Property] {
    (m in this.Maintenance)
}

pred World.DeleteMaintenanceRule_after[m:Property] {
    (m not in this.Maintenance)
}


fact BuildingRuleset  {
    all w, w' :World, b0:Object | ( 
        not( 
            (w' in w.next) 
            and ((b0 in w.Building) iff (b0 not in w'.Building))
        )
    )
}


fact CarRuleset  {
    all w, w' :World, c1:Object | ( 
        not( 
            (w' in w.next) 
            and ((c1 in w.Car) iff (c1 not in w'.Car))
        )
    )
}


fact RentalCompanyRuleset  {
    all w, w' :World, r2:Object | ( 
        not( 
            (w' in w.next) 
            and ((r2 in w.RentalCompany) iff (r2 not in w'.RentalCompany))
        )
    )
}


fact urgencyRuleset  {
    all w, w' :World, d2:Property | ( 
        (
			(w' in w.next) 
			and (
				((d2 in w.Damage) and (d2 in w'.Damage))
				and (d2.(w.urgency) != d2.(w'.urgency))
			)
		) => ( 
            (some int_:Int,int_0:Int |(w.[int_] and w'.[int_0]and (int_ = int_0)))
        )
    )
}

pred World.[int_:Int] {
    (invalid->int_ in this.urgency) 
}

pred World.[int_0:Int] {
    (invalid->int_0 in this.urgency) 
}


fact DamageRuleset_CreateDamageRule_example  {
    some w, w' :World, d:Property | (  
        (w' in w.next) and (some shared_r:Object |(w.CreateDamageRule_before[d, shared_r] and w'.CreateDamageRule_after[d, shared_r]))
    )
}
fact DamageRuleset_DeleteDamageRule_example  {
    some w, w' :World, d:Property | (  
        (w' in w.next) and (some shared_c:Object |(w.DeleteDamageRule_before[d, shared_c] and w'.DeleteDamageRule_after[d, shared_c]))
    )
}



fact RentalContractRuleset_CreateRentalContractRule_example  {
    some w, w' :World, r0:Property | (  
        (w' in w.next) and (some shared_r0:Object |(w.CreateRentalContractRule_before[r0, shared_r0] and w'.CreateRentalContractRule_after[r0, shared_r0]))
    )
}
fact RentalContractRuleset_DeleteRentalContractRule_example  {
    some w, w' :World, r0:Property | (  
        (w' in w.next) and ((w.DeleteRentalContractRule_before[r0] and w'.DeleteRentalContractRule_after[r0]))
    )
}

fact ParkingRuleset_CreateParkingRule_example  {
    some w, w' :World, p0:Property | (  
        (w' in w.next) and ((w.CreateParkingRule_before[p0] and w'.CreateParkingRule_after[p0]))
    )
}
fact ParkingRuleset_DeleteParkingRule_example  {
    some w, w' :World, p0:Property | (  
        (w' in w.next) and (some shared_r1:Object |(w.DeleteParkingRule_before[p0, shared_r1] and w'.DeleteParkingRule_after[p0, shared_r1]))
    )
}


fact PersonRuleset_CreatePersonRule_example  {
    some w, w' :World, p2:Object | (  
        (w' in w.next) and ((w.CreatePersonRule_before[p2] and w'.CreatePersonRule_after[p2]))
    )
}
fact PersonRuleset_DeletePersonRule_example  {
    some w, w' :World, p2:Object | (  
        (w' in w.next) and ((w.DeletePersonRule_before[p2] and w'.DeletePersonRule_after[p2]))
    )
}

fact MaintenanceRuleset_CreateMaintenanceRule_example  {
    some w, w' :World, m:Property | (  
        (w' in w.next) and (some shared_c0:Object |(w.CreateMaintenanceRule_before[m, shared_c0] and w'.CreateMaintenanceRule_after[m, shared_c0]))
    )
}
fact MaintenanceRuleset_DeleteMaintenanceRule_example  {
    some w, w' :World, m:Property | (  
        (w' in w.next) and ((w.DeleteMaintenanceRule_before[m] and w'.DeleteMaintenanceRule_after[m]))
    )
}




fact urgencyRuleset__example  {
    some w, w' :World, d2:Property | (  
        (w' in w.next) and (some int_:Int,int_0:Int |(w.[int_] and w'.[int_0]and (int_ = int_0)))
    )
}

